As hardware and software systems become more complex there is a growing need for automated formal verification methods. These methods are mathematically based techniques and languages that help detect and prevent design errors thereby avoiding losses in design effort and financial investment.
Examples of the type of properties being verified include safety properties (i.e. that the circuit can not enter undesirable states) and equivalence properties (i.e. that a high level model and the circuit being verified have equivalent behaviors). There are two well-established symbolic methods for automatically verifying such properties of circuits and finite state systems that are currently considered to be significant. The two most significant prior art methods are known as classical Symbolic Model Checking (SMC) and Symbolic Trajectory Evaluation (STE).
Classical SMC is more widely know and more widely received in the formal verification community. It involves building a finite model of a system as a set of states and state transitions and checking that a desired property holds in the model. An exhaustive search of all possible states of the model is performed in order to verify desired properties. The high level model can be expressed as temporal logic with the system having finite state transitions or as two automata that are compared according to some definition of equivalence. A representative of classical SMC from Carnegie Mellon University known as SMV (Symbolic Model Verifier) has been used for verifying circuit designs and protocols. Currently these techniques are being applied also to software verification.
One disadvantage associated with classical SMC is a problem known as state explosion. The state explosion problem is a failure characterized by exhaustion of computational resources because the required amount of computational resources expands according to the number of states defining the system. SMV, for example, is limited by the size of both the state space of systems and also the state space of properties being verified. Currently, classical SMC techniques are capable of verifying systems having hundreds of state encoding variables. The budget of state encoding variables must be used to describe both the high level model and the low level circuit or system. This limitation restricts classical SMC to verifying circuits up to functional unit block (FUB) levels. For systems with very much larger state spaces, SMC becomes impractical to use.
The second and less well-known technique, STE, is a lattice based model checking technique. It is more suitable for verifying properties of systems with very large state spaces (specifiable in thousands or tens of thousands of state encoding variables) because the number of variables required depends on the assertion being checked rather than on the system being verified. One significant drawback to STE lies in the specification language, which permits only a finite time period to be specified for a property.
A Generalized STE (GSTE) algorithm was proposed in a Ph.D. thesis by Alok Jain at Carnegie Mellon University in 1997. The GSTE proposed by Jain permits a class of complex safety properties with infinite time intervals to be specified and verified. One limitation to Jain's proposed GSTE is that it can only check for future possibilities based on some past and present state conditions. This capability is referred to as implication. For example, given a set of state conditions at some time, t, implication determines state conditions for time, t+1. Another, and possibly more important limitation is that the semantics of the extended specification language were not supported by rigorous theory. As a consequence few practitioners have understood and mastered the techniques required to use GSTE effectively.